High-assurance guards are often necessary for highly secure computer systems. However, in order to receive the desired “high-assurance” or “trusted” certification from government organizations such as the National Computer Security Center (NCSC), such guards must be subjected to an evaluation program (such as the Trusted Products Evaluation Program (TPEP)) in which they are tested against a comprehensive set of security-related criteria. Further, such evaluation typically requires construction and solution of complex mathematical proofs designed to prove the “correctness” of the guard being evaluated. Unfortunately, constructing and solving such proofs can make the evaluation process a complex, time-consuming and expensive undertaking.
Therefore, it may be desirable to have a system and method for providing a high-assurance guard for security applications which addresses the above-referenced problems and limitations of the current solutions.